A:Type, I:MaInterface(A), i:Id. ma-interface-loc(I;i)   

latex

Definitions

Void, t  T, x:A.B(x), Top, Type, a:A fp B(a), Id, b, s = t, type List, {x:A| B(x)} , x:A  B(x), Atom$n, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , ma-interface-dom(I;i), hasloc(k;i), Knd, left + right, x:AB(x), State(ds), IdDeq, x  dom(f), , x:A. B(x), strong-subtype(A;B), P  Q, S  T, (x  l), ma-interface-locs(I), [car / cdr], P  Q, P  Q, P & Q, P  Q, hd(l), last(L), l[i], MaInterface(T), x. t(x), f(x)?z, , x.A(x), null(as), b, ff, A, p =b q, i <z j, i z j, (i = j), x =a y, a < b, f(a), x f y, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, a = b, deq-member(eq;x;L), p  q, p  q, p q, tt, , Unit, ma-interface-loc(I;i), fpf-domain(f), a < b, x:A. B(x)

Lemmas

member-fpf-domain, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, not wf, fpf-dom wf, id-deq wf, bool wf, bfalse wf, bnot wf, null wf, null wf3, hasloc wf, ma-interface-dom wf, l member wf, ma-interface wf, decl-state wf, fpf-trivial-subtype-top, fpf wf, Id wf, l member subtype, member wf, top wf, assert wf, Knd wf, subtype rel wf